\subsection{Requirements Properties}
\label{sec:Running-Properties}

The requirements of \Sect \ref{sec:Running-Requirements} can now be formally expressed on the previous \textsc{Pn} as invariant formul\ae. Requirement \textbf{\texttt{R1}}, concerned with file opening by a sufficiently trusted user, is split into two properties $\mathtt{P1}$ and $\mathtt{P2}$, corresponding to each opening mode (resp. write / read mode). 

\begin{small}\hspace{-0.6cm}
$\begin{array}{r @{~\eqqdef~} l}
	\mathtt{P1}  & \forall~ \mathtt{\$p} = (\mathtt{\$f}, \mathtt{\$u}) \in \mathtt{write} \cdot \mathtt{ac_{u}} \rhd \mathtt{ac_{f}}\\
	\mathtt{P2}  & \forall~ \mathtt{\$p} = (\mathtt{\$f}, \mathtt{\$u}) \in \mathtt{read} \cdot \mathtt{ac_{u}} \rhd \mathtt{ac_{f}}\\
\end{array}$\end{small}

\smallskip\noindent
Here, requirement \textbf{\texttt{R1}} holds if for any pair $\mathtt{\$p} = (\mathtt{\$f}, \mathtt{\$u}) \in \mathtt{File}\times \mathtt{User}$ in the $\mathtt{write}$ or $\mathtt{read}$ place, $\mathtt{\$u}$'s access class dominates $\mathtt{\$f}$'s access class. Written in \Alpina, these two properties lead to the following \textsf{expression}s: 

\noindent
\begin{center}
	\begin{minipage}[b]{0.75\columnwidth}
		\setlistings{ADTlanguage}{0}
		\begin{lstlisting}{0}
Expressions
	P1: forall($p in write: userHasPermissionForFile($p)=true);
	P2: forall($p in read:  userHasPermissionForFile($p)=true);
Variables
	p : pair[file,user];
		\end{lstlisting}
	\end{minipage}
\end{center}



Requirement \textbf{\texttt{R2}} is implemented by a third property $\mathtt{P3}$ that ensures the confinement property on the \textsc{Pn}.

\smallskip
\hspace{-0.6cm}
\begin{small}
	$\mathtt{P3} ~\eqqdef \begin{array}{l}
		\forall~ \mathtt{\$p}=(\mathtt{\$f}, \mathtt{\$u})\in \mathtt{read}, \forall~ \mathtt{\$p'}=(\mathtt{\$f'}, \mathtt{\$u'})\in \mathtt{write} ~\cdot\\ \mathtt{\$un} = \mathtt{\$un'} \Longrightarrow \mathtt{\$ac_{f}} \rhd \mathtt{\$ac_f'}
	\end{array}$\end{small}


\smallskip\noindent
This property says that for all pairs of files simultaneously opened by the same user, when one is on read mode and the other on write mode, the read file's access class dominates the write file's one. Written in \Alpina, it gives the following \textsf{expression}:

\noindent
\begin{center}
	\begin{minipage}[b]{0.78\columnwidth}
		\setlistings{ADTlanguage}{0}
		\begin{lstlisting}{0}
Expressions
	P3: forall($p in read: 
		    forall ($p1 in write: 
			    (name(second($p1)) = name(second($p))) 
				  => 
				  !((class(first($p)) dominates class(first($p1))=true) &
				  !(name(first($p)) = name(first($p1))))
			  )
		  );
Variables
	p : pair[file,user];
	p1 : pair[file,user];
		\end{lstlisting}
	\end{minipage}
\end{center}


Running \Alpina on the naive \textsc{Fs} shows, as summarised in \Tab \ref{tab:satisfaction}, that none of these properties are satisfied: this \textsc{Fs} only implements as simple \textsc{Fs} mechanism without access control.



\begin{table}[t]%
\begin{center}
	\begin{tabular}{l c c c}
		 & \texttt{P1} & \texttt{P2} & \texttt{P3}\\
		\hline\hline
		\texttt{FS} & \tickNo & \tickNo & \tickNo\\
		\texttt{FS$_{\mathtt{s}}$} & \tickYes & \tickYes & \tickNo\\
		\texttt{FS$_{\mathtt{c}}$} & \tickYes & \tickYes & \tickYes\\
		\hline
	\end{tabular}
\end{center}
	\vspace{-.3cm}
	\caption{Property Satisfaction for the three \textsl{File System} versions.}
	\label{tab:satisfaction}
	
	\vspace{-.5cm}
\end{table}